Issue719.agda:11,23-24
Duplicate definition of module A. Previous definition of module A
at Issue719.agda:8,25-26
when scope checking the declaration
  open module A = M
